COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918  
C00026 ENDMK
C⊗;
(FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918  


     changes to:  IREWRITECOMS

     previous date: " 5-Jul-82 12:11:22" <CL.BOYER.LISPS>IREWRITE..3)


(PRETTYCOMPRINT IREWRITECOMS)

(RPAQQ IREWRITECOMS ((FNS * IREWRITEFNS)
	(PROP BLKLIBRARYDEF MEMBER)
	(BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST 
			      APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY 
			      ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME 
			      REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS 
			      SETUP TAUTOLOGYP TAUTP TEST 
			      TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP
			      (ENTRIES TEST SETUP)
			      (BLKLIBRARY EQUAL MEMBER GETPROP)
			      (GLOBALVARS TEMP-TEMP UNIFY-SUBST)))))

(RPAQQ IREWRITEFNS (ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST 
			      FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 
			      ONE-WAY-UNIFY1-LST PTIME REWRITE 
			      REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP 
			      TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES 
			      TRANS-OF-IMPLIES1 TRUEP))
(DEFINEQ

(ADD-LEMMA
  (LAMBDA (TERM)
    (COND
      ((AND (NOT (ATOM TERM))
	    (EQ (CAR TERM)
		(QUOTE EQUAL))
	    (NOT (ATOM (CADR TERM))))
	(COND
	  ((GETPROP (CAR (CADR TERM))
		    (QUOTE LEMMAS))
	    (PUTPROP (CAR (CADR TERM))
		     (QUOTE LEMMAS)
		     (CONS TERM (GETPROP (CAR (CADR TERM))
					 (QUOTE LEMMAS)))))
	  (T (SETPROPLIST (CAR (CADR TERM))
			  (CONS (QUOTE LEMMAS)
				(CONS (LIST TERM)
				      (GETPROPLIST (CAR (CADR TERM))))))
	     )))
      (T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
		TERM)))))

(ADD-LEMMA-LST
  (LAMBDA (LST)
    (COND
      ((NULL LST)
	T)
      (T (ADD-LEMMA (CAR LST))
	 (ADD-LEMMA-LST (CDR LST))))))

(APPLY-SUBST
  (LAMBDA (ALIST TERM)
    (COND
      ((NLISTP TERM)
	(COND
	  ((SETQ TEMP-TEMP (FASSOC TERM ALIST))
	    (CDR TEMP-TEMP))
	  (T TERM)))
      (T (CONS (CAR TERM)
	       (APPLY-SUBST-LST ALIST (CDR TERM)))))))

(APPLY-SUBST-LST
  (LAMBDA (ALIST LST)
    (COND
      ((NULL LST)
	NIL)
      (T (CONS (APPLY-SUBST ALIST (CAR LST))
	       (APPLY-SUBST-LST ALIST (CDR LST)))))))

(FALSEP
  (LAMBDA (X LST)
    (OR (EQUAL X (QUOTE (F)))
	(MEMBER X LST))))

(ONE-WAY-UNIFY
  (LAMBDA (TERM1 TERM2)
    (PROGN (SETQ UNIFY-SUBST NIL)
	   (ONE-WAY-UNIFY1 TERM1 TERM2))))

(ONE-WAY-UNIFY1
  (LAMBDA (TERM1 TERM2)
    (COND
      ((NLISTP TERM2)
	(COND
	  ((SETQ TEMP-TEMP (FASSOC TERM2 UNIFY-SUBST))
	    (EQUAL TERM1 (CDR TEMP-TEMP)))
	  (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
				     UNIFY-SUBST))
	     T)))
      ((ATOM TERM1)
	NIL)
      ((EQ (CAR TERM1)
	   (CAR TERM2))
	(ONE-WAY-UNIFY1-LST (CDR TERM1)
			    (CDR TERM2)))
      (T NIL))))

(ONE-WAY-UNIFY1-LST
  (LAMBDA (LST1 LST2)
    (COND
      ((NULL LST1)
	T)
      ((ONE-WAY-UNIFY1 (CAR LST1)
		       (CAR LST2))
	(ONE-WAY-UNIFY1-LST (CDR LST1)
			    (CDR LST2)))
      (T NIL))))

(PTIME
  (LAMBDA NIL
    (PROG (GCTM)
          (SETQ GCTM (CLOCK 3))
          (RETURN (CONS (IPLUS (CLOCK 2)
			       GCTM)
			GCTM)))))

(REWRITE
  (LAMBDA (TERM)
    (COND
      ((NLISTP TERM)
	TERM)
      (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
				    (REWRITE-ARGS (CDR TERM)))
			      (GETPROP (CAR TERM)
				       (QUOTE LEMMAS)))))))

(REWRITE-ARGS
  (LAMBDA (LST)
    (COND
      ((NULL LST)
	NIL)
      (T (CONS (REWRITE (CAR LST))
	       (REWRITE-ARGS (CDR LST)))))))

(REWRITE-WITH-LEMMAS
  (LAMBDA (TERM LST)
    (COND
      ((NULL LST)
	TERM)
      ((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
	(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
      (T (REWRITE-WITH-LEMMAS TERM (CDR LST))))))

(SETUP
  (LAMBDA NIL
    (ADD-LEMMA-LST
      (QUOTE
	((EQUAL (COMPILE FORM)
		(REVERSE (CODEGEN (OPTIMIZE FORM)
				  (NIL))))
	  (EQUAL (EQP X Y)
		 (EQUAL (FIX X)
			(FIX Y)))
	  (EQUAL (GREATERP X Y)
		 (LESSP Y X))
	  (EQUAL (LESSEQP X Y)
		 (NOT (LESSP Y X)))
	  (EQUAL (GREATEREQP X Y)
		 (NOT (LESSP X Y)))
	  (EQUAL (BOOLEAN X)
		 (OR (EQUAL X (T))
		     (EQUAL X (F))))
	  (EQUAL (IFF X Y)
		 (AND (IMPLIES X Y)
		      (IMPLIES Y X)))
	  (EQUAL (EVEN1 X)
		 (IF (ZEROP X)
		     (T)
		     (ODD (SUB1 X))))
	  (EQUAL (COUNTPS- L PRED)
		 (COUNTPS-LOOP L PRED (ZERO)))
	  (EQUAL (FACT- I)
		 (FACT-LOOP I 1))
	  (EQUAL (REVERSE- X)
		 (REVERSE-LOOP X (NIL)))
	  (EQUAL (DIVIDES X Y)
		 (ZEROP (REMAINDER Y X)))
	  (EQUAL (ASSUME-TRUE VAR ALIST)
		 (CONS (CONS VAR (T))
		       ALIST))
	  (EQUAL (ASSUME-FALSE VAR ALIST)
		 (CONS (CONS VAR (F))
		       ALIST))
	  (EQUAL (TAUTOLOGY-CHECKER X)
		 (TAUTOLOGYP (NORMALIZE X)
			     (NIL)))
	  (EQUAL (FALSIFY X)
		 (FALSIFY1 (NORMALIZE X)
			   (NIL)))
	  (EQUAL (PRIME X)
		 (AND (NOT (ZEROP X))
		      (NOT (EQUAL X (ADD1 (ZERO))))
		      (PRIME1 X (SUB1 X))))
	  (EQUAL (AND P Q)
		 (IF P (IF Q (T)
			   (F))
		     (F)))
	  (EQUAL (OR P Q)
		 (IF P (T)
		     (IF Q (T)
			 (F))
		     (F)))
	  (EQUAL (NOT P)
		 (IF P (F)
		     (T)))
	  (EQUAL (IMPLIES P Q)
		 (IF P (IF Q (T)
			   (F))
		     (T)))
	  (EQUAL (FIX X)
		 (IF (NUMBERP X)
		     X
		     (ZERO)))
	  (EQUAL (IF (IF A B C)
		     D E)
		 (IF A (IF B D E)
		     (IF C D E)))
	  (EQUAL (ZEROP X)
		 (OR (EQUAL X (ZERO))
		     (NOT (NUMBERP X))))
	  (EQUAL (PLUS (PLUS X Y)
		       Z)
		 (PLUS X (PLUS Y Z)))
	  (EQUAL (EQUAL (PLUS A B)
			(ZERO))
		 (AND (ZEROP A)
		      (ZEROP B)))
	  (EQUAL (DIFFERENCE X X)
		 (ZERO))
	  (EQUAL (EQUAL (PLUS A B)
			(PLUS A C))
		 (EQUAL (FIX B)
			(FIX C)))
	  (EQUAL (EQUAL (ZERO)
			(DIFFERENCE X Y))
		 (NOT (LESSP Y X)))
	  (EQUAL (EQUAL X (DIFFERENCE X Y))
		 (AND (NUMBERP X)
		      (OR (EQUAL X (ZERO))
			  (ZEROP Y))))
	  (EQUAL (MEANING (PLUS-TREE (APPEND X Y))
			  A)
		 (PLUS (MEANING (PLUS-TREE X)
				A)
		       (MEANING (PLUS-TREE Y)
				A)))
	  (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
			  A)
		 (FIX (MEANING X A)))
	  (EQUAL (APPEND (APPEND X Y)
			 Z)
		 (APPEND X (APPEND Y Z)))
	  (EQUAL (REVERSE (APPEND A B))
		 (APPEND (REVERSE B)
			 (REVERSE A)))
	  (EQUAL (TIMES X (PLUS Y Z))
		 (PLUS (TIMES X Y)
		       (TIMES X Z)))
	  (EQUAL (TIMES (TIMES X Y)
			Z)
		 (TIMES X (TIMES Y Z)))
	  (EQUAL (EQUAL (TIMES X Y)
			(ZERO))
		 (OR (ZEROP X)
		     (ZEROP Y)))
	  (EQUAL (EXEC (APPEND X Y)
		       PDS ENVRN)
		 (EXEC Y (EXEC X PDS ENVRN)
		       ENVRN))
	  (EQUAL (MC-FLATTEN X Y)
		 (APPEND (FLATTEN X)
			 Y))
	  (EQUAL (MEMBER X (APPEND A B))
		 (OR (MEMBER X A)
		     (MEMBER X B)))
	  (EQUAL (MEMBER X (REVERSE Y))
		 (MEMBER X Y))
	  (EQUAL (LENGTH (REVERSE X))
		 (LENGTH X))
	  (EQUAL (MEMBER A (INTERSECT B C))
		 (AND (MEMBER A B)
		      (MEMBER A C)))
	  (EQUAL (NTH (ZERO)
		      I)
		 (ZERO))
	  (EQUAL (EXP I (PLUS J K))
		 (TIMES (EXP I J)
			(EXP I K)))
	  (EQUAL (EXP I (TIMES J K))
		 (EXP (EXP I J)
		      K))
	  (EQUAL (REVERSE-LOOP X Y)
		 (APPEND (REVERSE X)
			 Y))
	  (EQUAL (REVERSE-LOOP X (NIL))
		 (REVERSE X))
	  (EQUAL (COUNT-LIST Z (SORT-LP X Y))
		 (PLUS (COUNT-LIST Z X)
		       (COUNT-LIST Z Y)))
	  (EQUAL (EQUAL (APPEND A B)
			(APPEND A C))
		 (EQUAL B C))
	  (EQUAL (PLUS (REMAINDER X Y)
		       (TIMES Y (QUOTIENT X Y)))
		 (FIX X))
	  (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
			     BASE)
		 (PLUS (POWER-EVAL L BASE)
		       I))
	  (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
			     BASE)
		 (PLUS I (PLUS (POWER-EVAL X BASE)
			       (POWER-EVAL Y BASE))))
	  (EQUAL (REMAINDER Y 1)
		 (ZERO))
	  (EQUAL (LESSP (REMAINDER X Y)
			Y)
		 (NOT (ZEROP Y)))
	  (EQUAL (REMAINDER X X)
		 (ZERO))
	  (EQUAL (LESSP (QUOTIENT I J)
			I)
		 (AND (NOT (ZEROP I))
		      (OR (ZEROP J)
			  (NOT (EQUAL J 1)))))
	  (EQUAL (LESSP (REMAINDER X Y)
			X)
		 (AND (NOT (ZEROP Y))
		      (NOT (ZEROP X))
		      (NOT (LESSP X Y))))
	  (EQUAL (POWER-EVAL (POWER-REP I BASE)
			     BASE)
		 (FIX I))
	  (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
				       (POWER-REP J BASE)
				       (ZERO)
				       BASE)
			     BASE)
		 (PLUS I J))
	  (EQUAL (GCD X Y)
		 (GCD Y X))
	  (EQUAL (NTH (APPEND A B)
		      I)
		 (APPEND (NTH A I)
			 (NTH B (DIFFERENCE I (LENGTH A)))))
	  (EQUAL (DIFFERENCE (PLUS X Y)
			     X)
		 (FIX Y))
	  (EQUAL (DIFFERENCE (PLUS Y X)
			     X)
		 (FIX Y))
	  (EQUAL (DIFFERENCE (PLUS X Y)
			     (PLUS X Z))
		 (DIFFERENCE Y Z))
	  (EQUAL (TIMES X (DIFFERENCE C W))
		 (DIFFERENCE (TIMES C X)
			     (TIMES W X)))
	  (EQUAL (REMAINDER (TIMES X Z)
			    Z)
		 (ZERO))
	  (EQUAL (DIFFERENCE (PLUS B (PLUS A C))
			     A)
		 (PLUS B C))
	  (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
			     Z)
		 (ADD1 Y))
	  (EQUAL (LESSP (PLUS X Y)
			(PLUS X Z))
		 (LESSP Y Z))
	  (EQUAL (LESSP (TIMES X Z)
			(TIMES Y Z))
		 (AND (NOT (ZEROP Z))
		      (LESSP X Y)))
	  (EQUAL (LESSP Y (PLUS X Y))
		 (NOT (ZEROP X)))
	  (EQUAL (GCD (TIMES X Z)
		      (TIMES Y Z))
		 (TIMES Z (GCD X Y)))
	  (EQUAL (VALUE (NORMALIZE X)
			A)
		 (VALUE X A))
	  (EQUAL (EQUAL (FLATTEN X)
			(CONS Y (NIL)))
		 (AND (NLISTP X)
		      (EQUAL X Y)))
	  (EQUAL (LISTP (GOPHER X))
		 (LISTP X))
	  (EQUAL (SAMEFRINGE X Y)
		 (EQUAL (FLATTEN X)
			(FLATTEN Y)))
	  (EQUAL (EQUAL (GREATEST-FACTOR X Y)
			(ZERO))
		 (AND (OR (ZEROP Y)
			  (EQUAL Y 1))
		      (EQUAL X (ZERO))))
	  (EQUAL (EQUAL (GREATEST-FACTOR X Y)
			1)
		 (EQUAL X 1))
	  (EQUAL (NUMBERP (GREATEST-FACTOR X Y))
		 (NOT (AND (OR (ZEROP Y)
			       (EQUAL Y 1))
			   (NOT (NUMBERP X)))))
	  (EQUAL (TIMES-LIST (APPEND X Y))
		 (TIMES (TIMES-LIST X)
			(TIMES-LIST Y)))
	  (EQUAL (PRIME-LIST (APPEND X Y))
		 (AND (PRIME-LIST X)
		      (PRIME-LIST Y)))
	  (EQUAL (EQUAL Z (TIMES W Z))
		 (AND (NUMBERP Z)
		      (OR (EQUAL Z (ZERO))
			  (EQUAL W 1))))
	  (EQUAL (GREATEREQPR X Y)
		 (NOT (LESSP X Y)))
	  (EQUAL (EQUAL X (TIMES X Y))
		 (OR (EQUAL X (ZERO))
		     (AND (NUMBERP X)
			  (EQUAL Y 1))))
	  (EQUAL (REMAINDER (TIMES Y X)
			    Y)
		 (ZERO))
	  (EQUAL (EQUAL (TIMES A B)
			1)
		 (AND (NOT (EQUAL A (ZERO)))
		      (NOT (EQUAL B (ZERO)))
		      (NUMBERP A)
		      (NUMBERP B)
		      (EQUAL (SUB1 A)
			     (ZERO))
		      (EQUAL (SUB1 B)
			     (ZERO))))
	  (EQUAL (LESSP (LENGTH (DELETE X L))
			(LENGTH L))
		 (MEMBER X L))
	  (EQUAL (SORT2 (DELETE X L))
		 (DELETE X (SORT2 L)))
	  (EQUAL (DSORT X)
		 (SORT2 X))
	  (EQUAL
	    (LENGTH (CONS X1
			  (CONS X2
				(CONS X3
				      (CONS X4 (CONS X5
						     (CONS X6 X7)))))))
	    (PLUS 6 (LENGTH X7)))
	  (EQUAL (DIFFERENCE (ADD1 (ADD1 X))
			     2)
		 (FIX X))
	  (EQUAL (QUOTIENT (PLUS X (PLUS X Y))
			   2)
		 (PLUS X (QUOTIENT Y 2)))
	  (EQUAL (SIGMA (ZERO)
			I)
		 (QUOTIENT (TIMES I (ADD1 I))
			   2))
	  (EQUAL (PLUS X (ADD1 Y))
		 (IF (NUMBERP Y)
		     (ADD1 (PLUS X Y))
		     (ADD1 X)))
	  (EQUAL (EQUAL (DIFFERENCE X Y)
			(DIFFERENCE Z Y))
		 (IF (LESSP X Y)
		     (NOT (LESSP Y Z))
		     (IF (LESSP Z Y)
			 (NOT (LESSP Y X))
			 (EQUAL (FIX X)
				(FIX Z)))))
	  (EQUAL (MEANING (PLUS-TREE (DELETE X Y))
			  A)
		 (IF (MEMBER X Y)
		     (DIFFERENCE (MEANING (PLUS-TREE Y)
					  A)
				 (MEANING X A))
		     (MEANING (PLUS-TREE Y)
			      A)))
	  (EQUAL (TIMES X (ADD1 Y))
		 (IF (NUMBERP Y)
		     (PLUS X (TIMES X Y))
		     (FIX X)))
	  (EQUAL (NTH (NIL)
		      I)
		 (IF (ZEROP I)
		     (NIL)
		     (ZERO)))
	  (EQUAL (LAST (APPEND A B))
		 (IF (LISTP B)
		     (LAST B)
		     (IF (LISTP A)
			 (CONS (CAR (LAST A))
			       B)
			 B)))
	  (EQUAL (EQUAL (LESSP X Y)
			Z)
		 (IF (LESSP X Y)
		     (EQUAL T Z)
		     (EQUAL F Z)))
	  (EQUAL (ASSIGNMENT X (APPEND A B))
		 (IF (ASSIGNEDP X A)
		     (ASSIGNMENT X A)
		     (ASSIGNMENT X B)))
	  (EQUAL (CAR (GOPHER X))
		 (IF (LISTP X)
		     (CAR (FLATTEN X))
		     (ZERO)))
	  (EQUAL (FLATTEN (CDR (GOPHER X)))
		 (IF (LISTP X)
		     (CDR (FLATTEN X))
		     (CONS (ZERO)
			   (NIL))))
	  (EQUAL (QUOTIENT (TIMES Y X)
			   Y)
		 (IF (ZEROP Y)
		     (ZERO)
		     (FIX X)))
	  (EQUAL (GET J (SET I VAL MEM))
		 (IF (EQP J I)
		     VAL
		     (GET J MEM))))))))

(TAUTOLOGYP
  (LAMBDA (X TRUE-LST FALSE-LST)
    (COND
      ((TRUEP X TRUE-LST)
	T)
      ((FALSEP X FALSE-LST)
	NIL)
      ((NLISTP X)
	NIL)
      ((EQ (CAR X)
	   (QUOTE IF))
	(COND
	  ((TRUEP (CADR X)
		  TRUE-LST)
	    (TAUTOLOGYP (CADDR X)
			TRUE-LST FALSE-LST))
	  ((FALSEP (CADR X)
		   FALSE-LST)
	    (TAUTOLOGYP (CADDDR X)
			TRUE-LST FALSE-LST))
	  (T (AND (TAUTOLOGYP (CADDR X)
			      (CONS (CADR X)
				    TRUE-LST)
			      FALSE-LST)
		  (TAUTOLOGYP (CADDDR X)
			      TRUE-LST
			      (CONS (CADR X)
				    FALSE-LST))))))
      (T NIL))))

(TAUTP
  (LAMBDA (X)
    (TAUTOLOGYP (REWRITE X)
		NIL NIL)))

(TEST
  (LAMBDA NIL
    (PROG (TM1 TM2 ANS TERM)
          (SETQ TM1 (PTIME))
          (SETQ TERM
	    (APPLY-SUBST
	      (QUOTE ((X F (PLUS (PLUS A B)
				 (PLUS C (ZERO))))
		       (Y F (TIMES (TIMES A B)
				   (PLUS C D)))
		       (Z F (REVERSE (APPEND (APPEND A B)
					     (NIL))))
		       (U EQUAL (PLUS A B)
			  (DIFFERENCE X Y))
		       (W LESSP (REMAINDER A B)
			  (MEMBER A (LENGTH B)))))
	      (QUOTE (IMPLIES (AND (IMPLIES X Y)
				   (AND (IMPLIES Y Z)
					(AND (IMPLIES Z U)
					     (IMPLIES U W))))
			      (IMPLIES X W)))))
          (SETQ ANS (TAUTP TERM))
          (SETQ TM2 (PTIME))
          (RETURN (LIST ANS (DIFFERENCE (CAR TM2)
					(CAR TM1))
			(DIFFERENCE (CDR TM2)
				    (CDR TM1)))))))

(TRANS-OF-IMPLIES
  (LAMBDA (N)
    (LIST (QUOTE IMPLIES)
	  (TRANS-OF-IMPLIES1 N)
	  (LIST (QUOTE IMPLIES)
		0 N))))

(TRANS-OF-IMPLIES1
  (LAMBDA (N)
    (COND
      ((EQUAL N 1)
	(LIST (QUOTE IMPLIES)
	      0 1))
      (T (LIST (QUOTE AND)
	       (LIST (QUOTE IMPLIES)
		     (SUB1 N)
		     N)
	       (TRANS-OF-IMPLIES1 (SUB1 N)))))))

(TRUEP
  (LAMBDA (X LST)
    (OR (EQUAL X (QUOTE (T)))
	(MEMBER X LST))))
)

(PUTPROPS MEMBER BLKLIBRARYDEF (LAMBDA
	    (.BLKVAR.X .BLKVAR.Y)
	    (DECLARE (LOCALVARS . T))
	    (PROG NIL LP (RETURN (COND ((NLISTP .BLKVAR.Y)
					NIL)
				       ((EQUAL .BLKVAR.X (CAR .BLKVAR.Y)
					       )
					.BLKVAR.Y)
				       (T (SETQ .BLKVAR.Y (CDR 
							  .BLKVAR.Y))
					  (GO LP)))))))
[DECLARE: DONTEVAL@LOAD DOEVAL@COMPILE DONTCOPY
(BLOCK: REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST 
	APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 
	ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS 
	REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST 
	TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP)
	(BLKLIBRARY EQUAL MEMBER GETPROP)
	(GLOBALVARS TEMP-TEMP UNIFY-SUBST))
]
STOP